\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, ${\it ks}$:Knd List,\+
\\[0ex]$a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$), $i$:Id.
\-\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal(${\it da}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)) $\in$ Id)
\\[0ex]$\Rightarrow$ msg{-}spec{-}loc{-}decl(${\it snd}$;$i$;${\it da}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. $k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ $\neg$$x$ $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ \=ecl{-}machine3(${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it snd}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=$\forall$$l$$\in$remove{-}repeats(IdLnkDeq;msg{-}spec{-}links(${\it snd}$)).\+
\\[0ex]es{-}decls(${\it es}$;source($l$);${\it ds}$ $\oplus$ $x$ : $T$;${\it da}$)
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ $\oplus$ $x$ : $T$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if \=deq{-}member(KindDeq;kind($e$);${\it ks}$)$\rightarrow$\+\+
\\[0ex]tagged{-}list{-}messages(\=(state when $e$);\+
\\[0ex]val($e$);
\\[0ex]ecl{-}m3($a$;${\it snd}$;$x$;$l$)(kind($e$)))
\-\-\\[0ex]else nil fi 
\-\\[0ex]and only these for tags in ecl{-}tags($l$;${\it snd}$)
\-\-\-
\end{tabbing}